Inference at * 1 
Iof proof for Lemma eq atom eq true elim sqequal:



1. x : Atom
2. y : Atom
  (x =a y ~ tt)  (x = y) 

latex

 by D 0 

latex

 1: 

 1: 3. x =a y ~ tt
 1:   x = y
 2: .....wf..... NILNIL

 2:   (x =a y ~ tt)  Type
 .

Definitions

P  Q, t  T